FDL - Nuprl Definition : existse-at

Nuprl Definition : existse-at

0,22

e@i.P(e) ==

e:E. loc(e) = i & P(e)

clarification:

existse-at(es; i; e.P(e)) ==

e:es-E(es). es-loc(es; e) = i

Id & P(e)

Definitions x:A. B(x), E, P & Q, s = t, Id, loc(e)

FDL editor aliases existse-at

Definitions	x:A. B(x), E, P & Q, s = t, Id, loc(e)
FDL editor aliases	existse-at